A, B:Realizer.
R-interface(A;B)

(i:Id.
(R-has-loc(B;i)
( kdom(R-da(B;i)). 

( T=R-da(B;i)(k)  
( Tisrcv(k)  destination(lnk(k)) = i  Id  R-da(A;source(lnk(k)))(k)?Void  T) 

latex

Definitions

Realizer, t  T, Knd, Top, x. t(x), x:A. B(x), a:A fp B(a), Type, x.A(x), R-da(R;i), x:AB(x), KindDeq, P  Q, f(x), Void, lnk(k), source(l), f(x)?z, destination(l), Id, s = t, isrcv(k), b, x  dom(f), R-has-loc(R;i), IdLnk, rcv(l,tg), Prop, P  Q, P & Q, P  Q, xdom(f). v=f(x)   P(x;v), R-interface(A;B), {T}, SQType(T), s ~ t, left+right, Atom$n, tag(k), False, A, b, , x:AB(x), Unit, EqDecider(T), x:A. B(x), rec(x.A(x)), if b t else f fi, Case b of inl(x)  s(x) ; inr(y)  t(y), f(a), lnk_rcv{lnk_rcv_compseq_tag_def:ObjectId}(tg; l), True, isrcv_rcv{isrcv_rcv_compseq_tag_def:ObjectId}(tg; l), P  Q, Dec(P)

Lemmas

decidable assert, not-R-has-loc-R-da, subtype rel self, deq wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, tagof wf, Id sq, isrcv-implies, Knd sq, rcv wf, IdLnk wf, R-has-loc wf, fpf-dom wf, assert wf, isrcv wf, Id wf, ldst wf, fpf-cap wf, lsrc wf, lnk wf, fpf-ap wf, Kind-deq wf, fpf-trivial-subtype-top, R-da wf, fpf wf, top wf, Knd wf, es realizer wf